(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 117))
(declare-fun v1 () (_ BitVec 90))
(declare-fun v2 () (_ BitVec 98))
(assert (let ((e3(_ bv121158448131738288543 67)))
(let ((e4 (bvcomp v0 ((_ sign_extend 27) v1))))
(let ((e5 (bvneg e4)))
(let ((e6 (bvnand v2 v2)))
(let ((e7 (bvshl v2 ((_ sign_extend 97) e4))))
(let ((e8 (bvmul v1 ((_ sign_extend 89) e4))))
(let ((e9 (bvnand ((_ sign_extend 97) e5) e6)))
(let ((e10 (ite (bvuge e5 e5) (_ bv1 1) (_ bv0 1))))
(let ((e11 (bvmul ((_ zero_extend 97) e4) v2)))
(let ((e12 ((_ extract 95 67) e9)))
(let ((e13 (bvurem e4 e5)))
(let ((e14 (bvlshr ((_ zero_extend 69) e12) e6)))
(let ((e15 (bvsrem ((_ sign_extend 23) e3) e8)))
(let ((e16 (bvsgt ((_ sign_extend 97) e10) v2)))
(let ((e17 (bvule ((_ zero_extend 97) e13) e11)))
(let ((e18 (bvsgt ((_ zero_extend 66) e13) e3)))
(let ((e19 (bvuge ((_ sign_extend 97) e13) e11)))
(let ((e20 (= ((_ sign_extend 89) e4) v1)))
(let ((e21 (bvugt ((_ sign_extend 23) e3) e8)))
(let ((e22 (bvule ((_ zero_extend 19) v2) v0)))
(let ((e23 (bvsgt e6 e14)))
(let ((e24 (distinct ((_ sign_extend 8) e15) v2)))
(let ((e25 (= e9 e6)))
(let ((e26 (bvslt ((_ sign_extend 27) v1) v0)))
(let ((e27 (distinct ((_ sign_extend 97) e5) e6)))
(let ((e28 (bvuge e14 ((_ sign_extend 8) v1))))
(let ((e29 (= e7 ((_ sign_extend 97) e13))))
(let ((e30 (bvsle e6 ((_ sign_extend 8) v1))))
(let ((e31 (distinct e3 ((_ sign_extend 66) e13))))
(let ((e32 (bvugt e6 e14)))
(let ((e33 (bvule e9 v2)))
(let ((e34 (= ((_ zero_extend 8) e8) e11)))
(let ((e35 (bvsgt e8 v1)))
(let ((e36 (bvult e11 ((_ sign_extend 97) e5))))
(let ((e37 (bvsle ((_ zero_extend 31) e3) e11)))
(let ((e38 (bvugt e11 ((_ zero_extend 97) e10))))
(let ((e39 (bvult ((_ sign_extend 8) v1) v2)))
(let ((e40 (bvsge v0 ((_ sign_extend 88) e12))))
(let ((e41 (= e23 e28)))
(let ((e42 (and e30 e17)))
(let ((e43 (and e20 e21)))
(let ((e44 (ite e33 e35 e40)))
(let ((e45 (or e32 e29)))
(let ((e46 (or e27 e22)))
(let ((e47 (or e19 e26)))
(let ((e48 (= e16 e44)))
(let ((e49 (or e48 e24)))
(let ((e50 (and e45 e47)))
(let ((e51 (xor e18 e18)))
(let ((e52 (not e34)))
(let ((e53 (and e37 e42)))
(let ((e54 (xor e51 e52)))
(let ((e55 (xor e50 e41)))
(let ((e56 (xor e55 e43)))
(let ((e57 (and e38 e53)))
(let ((e58 (xor e39 e31)))
(let ((e59 (and e54 e25)))
(let ((e60 (and e57 e49)))
(let ((e61 (=> e59 e58)))
(let ((e62 (= e56 e46)))
(let ((e63 (or e60 e36)))
(let ((e64 (= e63 e63)))
(let ((e65 (not e64)))
(let ((e66 (= e61 e65)))
(let ((e67 (not e62)))
(let ((e68 (xor e67 e67)))
(let ((e69 (or e68 e68)))
(let ((e70 (and e69 e69)))
(let ((e71 (not e66)))
(let ((e72 (and e70 e70)))
(let ((e73 (xor e71 e71)))
(let ((e74 (=> e72 e73)))
(let ((e75 (and e74 (not (= e8 (_ bv0 90))))))
(let ((e76 (and e75 (not (= e8 (bvnot (_ bv0 90)))))))
(let ((e77 (and e76 (not (= e5 (_ bv0 1))))))
e77
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
